i:Id, ds:x:Id fp Type, da:k:Knd fp Type, snd:msg-spec(ds;da). msg-spec-loc(snd;i)  Prop 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, msg-spec(ds;da), source(l), s = t, Prop, msg-spec-links(snd), IdLnk, (x  l), x:AB(x), P  Q, msg-spec-loc(snd;i)
Lemmas	l member wf, IdLnk wf, msg-spec-links wf, lsrc wf, msg-spec wf, Knd wf, fpf wf, Id wf